package net.za.cair.dip;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import net.za.cair.dip.model.MaterializationRanking;
import net.za.cair.dip.model.OntologyStructure;
import net.za.cair.dip.util.Permutation;
import net.za.cair.dip.util.Utility;

import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.AxiomType;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLDataFactory;
import org.semanticweb.owlapi.model.OWLIndividual;
import org.semanticweb.owlapi.model.OWLNamedIndividual;
import org.semanticweb.owlapi.model.OWLObjectPropertyAssertionAxiom;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyCreationException;
import org.semanticweb.owlapi.reasoner.OWLReasonerFactory;

/*
 * Copyright (C) 2011, Centre for Artificial Intelligence Research
 *
 * Modifications to the initial code base are copyright of their
 * respective authors, or their employers as appropriate.  Authorship
 * of the modifications may be determined from the ChangeLog placed at
 * the end of this file.
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.

 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.

 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301 USA
 */

/**
 * Author: Kody Moodley<br>
 * Centre for Artificial Intelligence Research<br>
 * UKZN and CSIR<br>
 * Date: 10-Oct-2011<br><br>
 */


public class ABoxToolBox {
	
	private OntologyStructure ontology;
	private OWLReasonerFactory reasonerFactory;
	private OWLDataFactory dataF = OWLManager.getOWLDataFactory();
	public ArrayList<Object[]> individualSequences;							//ABox: sequences of individual names in ontology
	public Set<OWLAxiom> uniqueABoxExtension;									//Unique ABox Extension if it exists
	public boolean uniqueABoxExtensionExists;									//Unique ABox Extension exists?
	
	public ABoxToolBox(OWLReasonerFactory reasonerFactory, OntologyStructure ontology){
		this.ontology = ontology;
		this.reasonerFactory = reasonerFactory;
		this.individualSequences = new ArrayList<Object[]>();
		this.uniqueABoxExtension = new HashSet<OWLAxiom>();
		this.uniqueABoxExtensionExists = false;
	}

	/*********************************************** ABOX SOLUTION ***********************************************/
	
	public boolean aBoxProcedure(MaterializationRanking ranking, OWLAxiom query, ArrayList<Object[]> indSequences) throws OWLOntologyCreationException{
		System.out.println("No of ranks: " + ranking.size());
		/**************Print out of steps for testing purposes****************/
		/*System.out.println(ranking);		
		System.out.println("assertions:");
		System.out.println("---------");
		Set<OWLAxiom> assertions = ontology.aBox.getAxioms();
		for (OWLAxiom as: assertions){
			System.out.println(man.render(as));
		}
		System.out.println();
		System.out.println("defaults:");
		System.out.println("---------");
		
		Set<OWLAxiom> defaults = ontology.dBox.getAxioms();
		for (OWLAxiom a: defaults){
			OWLSubClassOfAxiom s = (OWLSubClassOfAxiom)a;
			System.out.print(dlSyntaxRenderer.render(s.getSubClass()));
			System.out.print(" usually ");
			System.out.println(dlSyntaxRenderer.render(s.getSuperClass()));
		}
		System.out.println();
		/**********************************************************************/
		
		//OntologyStructure ontologyStructure = new OntologyStructure(ontology);
		Set<Set<OWLAxiom>> aBoxExtensions = new HashSet<Set<OWLAxiom>>();
		
		/************************************/
		/*System.out.println("extensions: ");
		System.out.println("-----------");
		/************************************/
		
		//int extensions = 1;
		//System.out.print("Extensions: ");
		/** For each sequence seq **/
		for (Object[] seq: indSequences){
			//System.out.print(extensions + ". ");
			Set<OWLAxiom> aBox = new HashSet<OWLAxiom>(ontology.aBox.getAxioms());
			
			/** For each individual in this particular sequence seq - apply procedure - to get ABox extension for seq. **/
			for (int j = 0; j < seq.length; j++){
				int i = 0;
				boolean done = false;
				OWLClassExpression currentDefault = null;
				OWLAxiom assertion = null;
				
				/** increment i while a default - d(i) = rank(i) u rank(i+1) u ... u rank(infinity) is NOT found 
				 * such that applying the materialization of this default to the current individual and adding the
				 * assertion to the KB preserves consistency. **/ 
				while (!done){
					//System.out.println("d(" + i + ")");
					
					currentDefault = ranking.getDefaultClassExpression(i);
					//System.out.println("Applying materialization default: " + dlSyntaxRenderer.render(currentDefault) + "\n to individual: " + man.render((OWLIndividual)seq[j]) + "...");
					assertion = dataF.getOWLClassAssertionAxiom(currentDefault, (OWLIndividual)seq[j]);
					//System.out.println(man.render(assertion));
					Set<OWLAxiom> tmpABox = new HashSet<OWLAxiom>(aBox);
					tmpABox.add(assertion);
					Set<OWLAxiom> tBox = new HashSet<OWLAxiom>();
					tBox.addAll(ontology.bBox.getAxioms());
					tBox.addAll(ontology.sBox.getAxioms());
					//tBox.addAll(ontologyStructure.dBox.getAxioms());
					if (Utility.getInstance().isConsistent(reasonerFactory, tmpABox, tBox)){
						//System.out.println("This operation keeps the TBox and ABox consistent.");
						done = true;
						aBox.add(assertion);				
					}
					else{
						//System.out.println("This operation makes the TBox and ABox inconsistent.");
					}
					if (i == ranking.size())
						done = true;						
					i++;
				}				
			}
			aBoxExtensions.add(aBox);
			//extensions++;
		}
		//System.out.println();
		
		/*******Multiple extension case: Check if query is entailed/contained in all the ABox extensions*****/
		for (Set<OWLAxiom> aBoxExtension: aBoxExtensions){
			if (!Utility.getInstance().containsAxiom(reasonerFactory, aBoxExtension, query)){
				return false;
			}
		}
		/****************************************************************************************************/
		return true;
	}
	
	/**ABox querying: optimization 1 - consider only individuals related to the queried one*/
	private Set<OWLIndividual> getCluster(Object[] individuals, Set<OWLObjectPropertyAssertionAxiom> axioms, OWLNamedIndividual queriedInd){
		Set<OWLIndividual> result = new HashSet<OWLIndividual>();
		
		/**Test: print all individuals and role assertions**/
		//Print out all individuals
		/*System.out.println("Individuals:");
		for (Object i: individuals)
			System.out.print(man.render((OWLNamedIndividual)i) + ", ");
		System.out.println();
		System.out.println();
		
		//Print out role assertions
		System.out.println("Assertions:");
				
		for (OWLObjectPropertyAssertionAxiom a: axioms)
			System.out.println(man.render(a));
		System.out.println();
		/**************************************************/
		
		//Translate asserted relations to boolean matrix
		int elements = individuals.length;
		int [][] relationMatrix = new int[elements][elements];
		for(int i=0; i < elements; i++){
		    for(int j=0; j < elements; j++){
		    	//1 if individuals[i] R individuals[j], else 0.
		    	int rel = 0;
		    	for (OWLObjectPropertyAssertionAxiom axiom: axioms){
		    		if (axiom.getSubject().equals(individuals[i]) && axiom.getObject().equals(individuals[j]))
		  				rel = 1;
		    	}
		    	relationMatrix[i][j]= rel;	
		  	}  
		}
		//Symmetric transformation
		for(int i=0; i < elements; i++){
		    for(int j=0; j < elements; j++){
		    	if (relationMatrix[i][j] == 1)
		    		relationMatrix[j][i]= 1;
		  	}  
		}
		//Transitive transformation
		int t1 = 0;int t2 = 0;
		for(int k=0; k < elements; k++){
			for(int i=0;i < elements; i++){
				for(int j=0; j < elements; j++){
		            t1=relationMatrix[i][k];
		            t2=relationMatrix[k][j];
		            if(t1 == 1 && t2 == 1)
		            	relationMatrix[i][j]=1;
		        }
		     }
		}
		//Read off the cluster from the matrix
		for(int i=0; i < elements; i++){
		    for(int j=0; j < elements; j++){
		    	if (relationMatrix[i][j] == 1){
		    		if (individuals[i] == queriedInd)
		    			result.add((OWLIndividual)individuals[j]);
		    		if (individuals[j] == queriedInd)
		    			result.add((OWLIndividual)individuals[i]);
		    	}	
		  	}  
		}
		result.add(queriedInd); //cluster has to at least contain the queried individual
		
		/**Test: print relevant cluster**/
		/*System.out.println("Cluster:");
				
		for (OWLIndividual c: result)
			System.out.print(man.render(c) + ", ");
		System.out.println();
		System.out.println();
		/*******************************/
		
		//Return set of relevant individuals to queried individual
		return result;
	}
	
	private Set<OWLAxiom> uniqueExtension(MaterializationRanking ranking, OWLOntology ontology, OWLNamedIndividual queriedInd) throws OWLOntologyCreationException{
		/**Find largest default to apply to each individual in the cluster (separately)
		 * If you add the corresponding assertion to the abox and it preserves consistency
		 * of the KB (for ALL individuals in the cluster) then there is a unique extension
		 * of the ABox and the unique extension is A U {d(indiv)} for all indiv in cluster.
		 */
		OntologyStructure structure = new OntologyStructure(ontology);
		//Get relevant cluster
		Set<OWLIndividual> cluster = getCluster(ontology.getIndividualsInSignature().toArray(), ontology.getAxioms(AxiomType.OBJECT_PROPERTY_ASSERTION), queriedInd);
		
		Set<OWLAxiom> compatibleDefaultAssertions = new HashSet<OWLAxiom>();
		//No need to compute ALL the sequences
		/** For each individual in this particular sequence seq - apply procedure - to get ABox extension for seq. **/
		for (OWLIndividual ind: cluster){
			int i = 0;
			boolean done = false;
			OWLClassExpression currentDefault = null;
			OWLAxiom assertion = null;
			
			/** increment i while a default - d(i) = rank(i) u rank(i+1) u ... u rank(infinity) is NOT found 
			 * such that applying the materialization of this default to the current individual and adding the
			 * assertion to the KB preserves consistency. **/ 
			while (!done){
				currentDefault = ranking.getDefaultClassExpression(i);
				assertion = dataF.getOWLClassAssertionAxiom(currentDefault, (OWLIndividual)ind);
				Set<OWLAxiom> tmpABox = new HashSet<OWLAxiom>(structure.aBox.getAxioms());
				tmpABox.add(assertion);
				Set<OWLAxiom> tBox = new HashSet<OWLAxiom>();
				tBox.addAll(structure.bBox.getAxioms());
				tBox.addAll(structure.sBox.getAxioms());
				//tBox.addAll(ontologyStructure.dBox.getAxioms());
				if (!Utility.getInstance().isConsistent(reasonerFactory, tmpABox, tBox)){
					//There is no unique extension
					return new HashSet<OWLAxiom>();		
				}
				else{
					done = true;
					compatibleDefaultAssertions.add(assertion);	
				}
				if (i == ranking.size())
					done = true;						
				i++;
			}				
		}
		
		/**Check if <T, D, A U compatibleDefaultAssertions> is consistent.
		 * If it is: then unique extension exists (return A U compatibleDefaultAssertions).
		 * Else: unique extension does not exist (return empty set).
		 */
		//TBox
		Set<OWLAxiom> tBox = new HashSet<OWLAxiom>();
		tBox.addAll(structure.bBox.getAxioms());
		tBox.addAll(structure.sBox.getAxioms());
		//ABox
		compatibleDefaultAssertions.addAll(structure.aBox.getAxioms()); //A U compatibleDefaultAssertions
		Set<OWLAxiom> tmpABox = new HashSet<OWLAxiom>(compatibleDefaultAssertions);
		
		if (Utility.getInstance().isConsistent(reasonerFactory, tmpABox, tBox)) //unique extension exists
			return tmpABox;
		
		return new HashSet<OWLAxiom>();//multiple extensions
	}
	
	private void generateIndividualSequences(OWLOntology ontology, OWLNamedIndividual queriedInd){
		Set<OWLNamedIndividual> ind = ontology.getIndividualsInSignature();
		/************************************************More than one individual*****************************************************/
		if (ind.size() > 1){
			Set<OWLIndividual> cluster = getCluster(ind.toArray(), ontology.getAxioms(AxiomType.OBJECT_PROPERTY_ASSERTION), queriedInd);
			//System.out.println("Cluster size: " + cluster.size());
			Object [] individuals = cluster.toArray();
			
			//Generate all sequences of the individuals
			Iterator<?> i = new Permutation(individuals);
			individualSequences = new ArrayList<Object[]>();
			while (i.hasNext()){
				int count = 0;
				Object[] t = new Object[individuals.length];
				for (Object s: (Object[])i.next()){
					t[count] = s;
					count++;
				}
				individualSequences.add(t);
			}
		}
		/*************************************************Only one individual**********************************************************/
		else{
			individualSequences = new ArrayList<Object[]>();
			Object[] t = new Object[ind.size()];
			int count = 0;
			for (OWLNamedIndividual ni: ind){
				t[count] = ni;
				count++;
			}
			individualSequences.add(t);
		}
		/**************************************Print the sequences to console for testing**********************************************/
		//printSequences(individualSequences);
	}
	
	public void prepareABoxResources(MaterializationRanking ranking, OWLOntology ontology, OWLNamedIndividual queriedInd) throws OWLOntologyCreationException{
		/**Generate relevant cluster of individuals and all sequences thereof**/
		generateIndividualSequences(ontology, queriedInd);
		
		/**Determine if there is a unique extension of the ABox**/
		uniqueABoxExtension = uniqueExtension(ranking, ontology, queriedInd);
		
		if (uniqueABoxExtension.size() > 0){
			/**There is a unique ABox extension**/
			uniqueABoxExtensionExists = true;
		}
	}
}
